COMMENT ⊗   VALID 00004 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	 bird.lsp[w84,jmc]	Bird circumscription in ekl
C00006 00003	1. (DEFINE A
C00012 00004	(get-proofs bird prf s84 jmc)
C00027 ENDMK
C⊗;
;;; bird.lsp[w84,jmc]	Bird circumscription in ekl

(proof bird)

1. (define a |∀ab flies.a(ab,flies) ≡ 

(∀x.¬ab aspect1 x ⊃ ¬flies x)

∧ (∀x.bird x ⊃ ab aspect1 x)

∧ (∀x.bird x ∧ ¬ab aspect2 x ⊃ flies x)

∧ (∀x.ostrich x ⊃ ab aspect2 x)

∧ (∀x.ostrich x ∧ ¬ab aspect3 x ⊃ ¬flies x)

|)

2. (axiom |
(∀x y.¬(aspect1 x = aspect2 y))

∧ (∀x y.¬(aspect1 x = aspect3 y))

∧ (∀x y.¬(aspect2 x = aspect3 y))

∧ (∀x y.aspect1 x = aspect1 y ≡ x =y)

∧ (∀x y.aspect2 x = aspect2 y ≡ x =y)

∧ (∀x y.aspect3 x = aspect3 y ≡ x =y)

|)
(label simpinfo)

3. (define a1 |∀ab flies.a1(ab,flies) ≡ a(ab,flies) ∧ 
		∀ab1 flies1.(a(ab1,flies1) ∧ (∀z.ab1 z ⊃ ab z)
			⊃ (∀z.ab z ≡ ab1 z))|)

4. (assume |a1(ab,flies)|)

5. (define flies2 |∀x.flies2 x ≡ bird x ∧ ¬ostrich x|)

6. (define ab2 |∀z.ab2 z ≡ (∃x.bird x ∧ z = aspect1 x)
	∨ (∃x.ostrich x ∧ z = aspect2 x)|)

7. (rw 4 (open a1))

8. (trw bird#7#1 7)

9. (trw bird#7#2 7)

10. (rw 8 (open a))

11. (assume |ab2 z|)

12. (rw * (open ab2))

13. (derive |ab z| (12 10))

14. (ci (11) 13)

15. (der |∀z.ab2 z ⊃ ab z| 14)

16. (der |∀x.¬ab2 aspect1 x ⊃ ¬flies2 x| (5 6))

17. (der |∀x.bird x ⊃ ab2 aspect1 x| (5 6))

18. (der |∀x.bird x ∧ ¬ab2 aspect2 x ⊃ flies2 x| (5 6))

19. (der |∀x.ostrich x ⊃ ab2 aspect2 x| (5 6))

;(der |∀x.ostrich x ∧ ¬ab2 aspect3 x ⊃ ¬flies2 x| (5 6))
; This is the one that causes PDL overflow, but breaking it in two works.

20. (der |∀x.ostrich x ⊃ ¬flies2 x| (5 6))

21. (der |∀x.ostrich x ∧ ¬ab2 aspect3 x ⊃ ¬flies2 x| *)
; 20 and 21 should be one step

22. (der |bird#16∧bird#17∧bird#18∧bird#19∧bird#21| (16:21))

23. (ue ((ab.ab2) (flies.flies2)) 1)

24. (rw 23 (use 22))

25. (der |∀z.ab z ≡ AB2 Z| (9 15 24))

26. (rw 8 (use 1 mode: exact) ((use 25 mode: exact) (open ab2)))

27. (der |∀x.flies x ≡ bird x ∧ ¬ostrich x| 26)

(save-proofs bird prf s84 jmc)
1. (DEFINE A
     |∀AB FLIES.A(AB,FLIES)≡
                (∀X.¬AB(ASPECT1(X))⊃¬FLIES(X))∧(∀X.BIRD(X)⊃AB(ASPECT1(X)))∧
                (∀X.BIRD(X)∧¬AB(ASPECT2(X))⊃FLIES(X))∧
                (∀X.OSTRICH(X)⊃AB(ASPECT2(X)))∧
                (∀X.OSTRICH(X)∧¬AB(ASPECT3(X))⊃¬FLIES(X))| NIL)

;labels: SIMPINFO 
2. (AXIOM
     |(∀X Y.¬ASPECT1(X)=ASPECT2(Y))∧(∀X Y.¬ASPECT1(X)=ASPECT3(Y))∧
      (∀X Y.¬ASPECT2(X)=ASPECT3(Y))∧(∀X Y.ASPECT1(X)=ASPECT1(Y)≡X=Y)∧
      (∀X Y.ASPECT2(X)=ASPECT2(Y)≡X=Y)∧(∀X Y.ASPECT3(X)=ASPECT3(Y)≡X=Y)|)

3. (DEFINE A1
     |∀AB FLIES.A1(AB,FLIES)≡
                A(AB,FLIES)∧
                (∀AB1 FLIES1.A(AB1,FLIES1)∧(∀Z.AB1(Z)⊃AB(Z))⊃(∀Z.AB(Z)≡AB1(Z)))|
     NIL)

4. (ASSUME |A1(AB,FLIES)|)
deps: (4)

5. (DEFINE FLIES2 |∀X.FLIES2(X)≡BIRD(X)∧¬OSTRICH(X)| NIL)

6. (DEFINE AB2
     |∀Z.AB2(Z)≡(∃X.BIRD(X)∧Z=ASPECT1(X))∨(∃X.OSTRICH(X)∧Z=ASPECT2(X))| 
NIL)

7. (RW 4 (OPEN A1))
A(AB,FLIES)∧(∀AB1 FLIES1.A(AB1,FLIES1)∧(∀Z.AB1(Z)⊃AB(Z))⊃(∀Z.AB(Z)≡AB1(Z)))
deps: (4)

8. (TRW |A(AB,FLIES)| (USE 7))
A(AB,FLIES)
deps: (4)

9. (TRW |∀AB1 FLIES1.A(AB1,FLIES1)∧(∀Z.AB1(Z)⊃AB(Z))⊃(∀Z.AB(Z)≡AB1(Z))| 
(USE 7))
∀AB1 FLIES1.A(AB1,FLIES1)∧(∀Z.AB1(Z)⊃AB(Z))⊃(∀Z.AB(Z)≡AB1(Z))
deps: (4)

10. (RW 8 (OPEN A))
(∀X.¬AB(ASPECT1(X))⊃¬FLIES(X))∧(∀X.BIRD(X)⊃AB(ASPECT1(X)))∧
(∀X.BIRD(X)∧¬AB(ASPECT2(X))⊃FLIES(X))∧(∀X.OSTRICH(X)⊃AB(ASPECT2(X)))∧
(∀X.OSTRICH(X)∧¬AB(ASPECT3(X))⊃¬FLIES(X))
deps: (4)

11. (ASSUME |AB2(Z)|)
deps: (11)

12. (RW 11 (OPEN AB2))
(∃X.BIRD(X)∧Z=ASPECT1(X))∨(∃X.OSTRICH(X)∧Z=ASPECT2(X))
deps: (11)

13. (DERIVE |AB(Z)| (12 10) NIL)
AB(Z)
deps: (4 11)

14. (CI (11) 13 NIL)
AB2(Z)⊃AB(Z)
deps: (4)

15. (DERIVE |∀Z.AB2(Z)⊃AB(Z)| (14) NIL)
∀Z.AB2(Z)⊃AB(Z)
deps: (4)

16. (DERIVE |∀X.¬AB2(ASPECT1(X))⊃¬FLIES2(X)| (5 6) NIL)
∀X.¬AB2(ASPECT1(X))⊃¬FLIES2(X)

17. (DERIVE |∀X.BIRD(X)⊃AB2(ASPECT1(X))| (5 6) NIL)
∀X.BIRD(X)⊃AB2(ASPECT1(X))

18. (DERIVE |∀X.BIRD(X)∧¬AB2(ASPECT2(X))⊃FLIES2(X)| (5 6) NIL)
∀X.BIRD(X)∧¬AB2(ASPECT2(X))⊃FLIES2(X)

19. (DERIVE |∀X.OSTRICH(X)⊃AB2(ASPECT2(X))| (5 6) NIL)
∀X.OSTRICH(X)⊃AB2(ASPECT2(X))

20. (DERIVE |∀X.OSTRICH(X)⊃¬FLIES2(X)| (5 6) NIL)
∀X.OSTRICH(X)⊃¬FLIES2(X)

21. (DERIVE |∀X.OSTRICH(X)∧¬AB2(ASPECT3(X))⊃¬FLIES2(X)| (20) NIL)
∀X.OSTRICH(X)∧¬AB2(ASPECT3(X))⊃¬FLIES2(X)

22. (DERIVE
      |(∀X.¬AB2(ASPECT1(X))⊃¬FLIES2(X))∧(∀X.BIRD(X)⊃AB2(ASPECT1(X)))∧
       (∀X.BIRD(X)∧¬AB2(ASPECT2(X))⊃FLIES2(X))∧(∀X.OSTRICH(X)⊃AB2(ASPECT2(X)))∧
       (∀X.OSTRICH(X)∧¬AB2(ASPECT3(X))⊃¬FLIES2(X))| (16 17 18 19 20 21) 
NIL)
(∀X.¬AB2(ASPECT1(X))⊃¬FLIES2(X))∧(∀X.BIRD(X)⊃AB2(ASPECT1(X)))∧
(∀X.BIRD(X)∧¬AB2(ASPECT2(X))⊃FLIES2(X))∧(∀X.OSTRICH(X)⊃AB2(ASPECT2(X)))∧
(∀X.OSTRICH(X)∧¬AB2(ASPECT3(X))⊃¬FLIES2(X))

23. (UE ((AB.|AB2|) (FLIES.|FLIES2|)) 1 NIL)
A(AB2,FLIES2)≡
(∀X.¬AB2(ASPECT1(X))⊃¬FLIES2(X))∧(∀X.BIRD(X)⊃AB2(ASPECT1(X)))∧
(∀X.BIRD(X)∧¬AB2(ASPECT2(X))⊃FLIES2(X))∧(∀X.OSTRICH(X)⊃AB2(ASPECT2(X)))∧
(∀X.OSTRICH(X)∧¬AB2(ASPECT3(X))⊃¬FLIES2(X))

24. (RW 23 (USE 22))
A(AB2,FLIES2)

25. (DERIVE |∀Z.AB(Z)≡AB2(Z)| (9 15 24) NIL)
∀Z.AB(Z)≡AB2(Z)
deps: (4)

26. (RW 8 ((USE 1 MODE: EXACT) ((USE 25 MODE: EXACT) (OPEN AB2))))
(∀X.¬(∃X1.BIRD(X1)∧X=X1)⊃¬FLIES(X))∧
(∀X.BIRD(X)∧¬(∃X2.OSTRICH(X2)∧X=X2)⊃FLIES(X))∧(∀X.OSTRICH(X)⊃¬FLIES(X))
deps: (4)

27. (DERIVE |∀X.FLIES(X)≡BIRD(X)∧¬OSTRICH(X)| (26) NIL)
∀X.FLIES(X)≡BIRD(X)∧¬OSTRICH(X)
deps: (4)

28. 
(get-proofs bird prf s84 jmc)
(ttyekl)
(show)

1. (DEFINE A
     |ALL AB FLIES.A(AB,FLIES) IFF 
                   (ALL X.NOT AB(ASPECT1(X)) IMP NOT FLIES(X))&
                   (ALL X.BIRD(X) IMP AB(ASPECT1(X)))&
                   (ALL X.BIRD(X)&NOT AB(ASPECT2(X)) IMP FLIES(X))&
                   (ALL X.OSTRICH(X) IMP AB(ASPECT2(X)))&
                   (ALL X.OSTRICH(X)&NOT AB(ASPECT3(X)) IMP NOT FLIES(X))| 
NIL)

;labels: SIMPINFO 
2. (AXIOM
     |(ALL X Y.NOT ASPECT1(X)=ASPECT2(Y))&(ALL X Y.NOT ASPECT1(X)=ASPECT3(Y))&
      (ALL X Y.NOT ASPECT2(X)=ASPECT3(Y))&
      (ALL X Y.ASPECT1(X)=ASPECT1(Y) IFF X=Y)&
      (ALL X Y.ASPECT2(X)=ASPECT2(Y) IFF X=Y)&
      (ALL X Y.ASPECT3(X)=ASPECT3(Y) IFF X=Y)|)

3. (DEFINE A1
     |ALL AB FLIES.A1(AB,FLIES) IFF 
                   A(AB,FLIES)&
                   (ALL AB1 FLIES1.A(AB1,FLIES1)&(ALL Z.AB1(Z) IMP AB(Z)) 
IMP 
                                   (ALL Z.AB(Z) IFF AB1(Z)))| NIL)

4. (ASSUME |A1(AB,FLIES)|)
deps: (4)

5. (DEFINE FLIES2 |ALL X.FLIES2(X) IFF BIRD(X)&NOT OSTRICH(X)| NIL)

6. (DEFINE AB2
     |ALL Z.AB2(Z) IFF 
            (EX X.BIRD(X)&Z=ASPECT1(X)) OR (EX X.OSTRICH(X)&Z=ASPECT2(X))| 
NIL)

7. (RW 4 (USE 3 MODE: EXACT))
A(AB,FLIES)&
(ALL AB1 FLIES1.A(AB1,FLIES1)&(ALL Z.AB1(Z) IMP AB(Z)) IMP 
                (ALL Z.AB(Z) IFF AB1(Z)))
deps: (4)

8. (TRW |A(AB,FLIES)| (USE 7))
A(AB,FLIES)
deps: (4)

9. (TRW
     |ALL AB1 FLIES1.A(AB1,FLIES1)&(ALL Z.AB1(Z) IMP AB(Z)) IMP 
                     (ALL Z.AB(Z) IFF AB1(Z))| (USE 7))
ALL AB1 FLIES1.A(AB1,FLIES1)&(ALL Z.AB1(Z) IMP AB(Z)) IMP 
               (ALL Z.AB(Z) IFF AB1(Z))
deps: (4)

10. (RW 8 (USE 1 MODE: EXACT))
(ALL X.NOT AB(ASPECT1(X)) IMP NOT FLIES(X))&(ALL X.BIRD(X) IMP AB(ASPECT1(X)))&
(ALL X.BIRD(X)&NOT AB(ASPECT2(X)) IMP FLIES(X))&
(ALL X.OSTRICH(X) IMP AB(ASPECT2(X)))&
(ALL X.OSTRICH(X)&NOT AB(ASPECT3(X)) IMP NOT FLIES(X))
deps: (4)

11. (ASSUME |AB2(Z)|)
deps: (11)

12. (RW 11 (OPEN AB2))
(EX X.BIRD(X)&Z=ASPECT1(X)) OR (EX X.OSTRICH(X)&Z=ASPECT2(X))
deps: (11)

13. (DERIVE |AB(Z)| (12 10) NIL)
AB(Z)
deps: (4 11)

14. (CI (11) 13 NIL)
AB2(Z) IMP AB(Z)
deps: (4)

15. (DERIVE |ALL Z.AB2(Z) IMP AB(Z)| (14) NIL)
ALL Z.AB2(Z) IMP AB(Z)
deps: (4)

16. (DERIVE |ALL X.NOT AB2(ASPECT1(X)) IMP NOT FLIES2(X)| (5 6) NIL)
ALL X.NOT AB2(ASPECT1(X)) IMP NOT FLIES2(X)

17. (DERIVE |ALL X.BIRD(X) IMP AB2(ASPECT1(X))| (5 6) NIL)
ALL X.BIRD(X) IMP AB2(ASPECT1(X))

18. (DERIVE |ALL X.BIRD(X)&NOT AB2(ASPECT2(X)) IMP FLIES2(X)| (5 6) NIL)
ALL X.BIRD(X)&NOT AB2(ASPECT2(X)) IMP FLIES2(X)

19. (DERIVE |ALL X.OSTRICH(X) IMP AB2(ASPECT2(X))| (5 6) NIL)
ALL X.OSTRICH(X) IMP AB2(ASPECT2(X))

20. (DERIVE |ALL X.OSTRICH(X) IMP NOT FLIES2(X)| (5 6) NIL)
ALL X.OSTRICH(X) IMP NOT FLIES2(X)

21. (DERIVE |ALL X.OSTRICH(X)&NOT AB2(ASPECT3(X)) IMP NOT FLIES2(X)| (20) 
NIL)
ALL X.OSTRICH(X)&NOT AB2(ASPECT3(X)) IMP NOT FLIES2(X)

22. (DERIVE
      |(ALL X.NOT AB2(ASPECT1(X)) IMP NOT FLIES2(X))&
       (ALL X.BIRD(X) IMP AB2(ASPECT1(X)))&
       (ALL X.BIRD(X)&NOT AB2(ASPECT2(X)) IMP FLIES2(X))&
       (ALL X.OSTRICH(X) IMP AB2(ASPECT2(X)))&
       (ALL X.OSTRICH(X)&NOT AB2(ASPECT3(X)) IMP NOT FLIES2(X))|
      (16 17 18 19 20 21) NIL)
(ALL X.NOT AB2(ASPECT1(X)) IMP NOT FLIES2(X))&
(ALL X.BIRD(X) IMP AB2(ASPECT1(X)))&
(ALL X.BIRD(X)&NOT AB2(ASPECT2(X)) IMP FLIES2(X))&
(ALL X.OSTRICH(X) IMP AB2(ASPECT2(X)))&
(ALL X.OSTRICH(X)&NOT AB2(ASPECT3(X)) IMP NOT FLIES2(X))

23. (UE ((AB.|AB2|) (FLIES.|FLIES2|)) 1 NIL)
A(AB2,FLIES2) IFF 
(ALL X.NOT AB2(ASPECT1(X)) IMP NOT FLIES2(X))&
(ALL X.BIRD(X) IMP AB2(ASPECT1(X)))&
(ALL X.BIRD(X)&NOT AB2(ASPECT2(X)) IMP FLIES2(X))&
(ALL X.OSTRICH(X) IMP AB2(ASPECT2(X)))&
(ALL X.OSTRICH(X)&NOT AB2(ASPECT3(X)) IMP NOT FLIES2(X))

24. (RW 23 (USE 22))
A(AB2,FLIES2)

25. (DERIVE |ALL Z.AB(Z) IFF AB2(Z)| (9 15 24) NIL)
ALL Z.AB(Z) IFF AB2(Z)
deps: (4)

26. (RW 8 ((USE 1 MODE: EXACT) ((USE 25 MODE: EXACT) (OPEN AB2))))
(ALL X.NOT (EX X1.BIRD(X1)&X=X1) IMP NOT FLIES(X))&
(ALL X.BIRD(X)&NOT (EX X2.OSTRICH(X2)&X=X2) IMP FLIES(X))&
(ALL X.OSTRICH(X) IMP NOT FLIES(X))
deps: (4)

27. (DERIVE |ALL X.FLIES(X) IFF BIRD(X)&NOT OSTRICH(X)| (26) NIL)
ALL X.FLIES(X) IFF BIRD(X)&NOT OSTRICH(X)
deps: (4)

28.